i, a:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp).
Normal(T)
 Normal(ds)
 (s:State(ds). Dec(v:T. P(s,v)))
 @i precondition for a(v:T):P State(ds) v ||- es.@i Precondition for a(v)P State(ds) (v:T) 

latex

Definitions	es realizer ind Rpre compseq tag def, Consistent(R;es), ES, t  T, x:A. B(x), @loc precondition for a(v:T):P State(ds) v, @i Precondition for a(v)P State(ds) (v:T), x:AB(x), P  Q, A & B, P & Q, R-Feasible(R), inr(x), x:AB(x), R ||- es.P(es), Id, Type, x. t(x), a:A fp B(a), Prop, State(ds), Normal(T), Normal(ds), f(a), x:A. B(x), Dec(P)
Lemmas	decidable wf, normal-ds wf, normal-type wf, decl-state wf, fpf wf, Id wf, R-consistent wf, Rpre wf, event system wf